es:ES, A:Type, i:Id, ds:x:Id fp Type, conds:k:Knd fp V:Type  (State(ds)V(A + Top)), e:E.
(e:E.
(loc(e) = i)
 (kind(e)  dom(conds))
 ((valtype(e) r (conds(kind(e)).1)) & (state@loc(e) r State(ds))))
 ((e  es-triggers(es;i;ds;conds)))
 (es-triggers(es;i;ds;conds)(e) ~ outl((conds(kind(e)).2)((state when e),val(e)))) 

latex

Definitions

False, t  T, x:A. B(x), P  Q, P  Q, b, ff, valtype(e), Type, State(ds), Top, left + right, x:AB(x), Knd, x:A  B(x), f(x), t.1, val(e), state@i, (state when e), x. t(x), t.2, f(a), isl(x), P & Q, , s ~ t, {T}, outl(x), <a, b>, s = t, , SQType(T), x.A(x), A, True, b, Id, p q, T, P  Q, P  Q, Unit, do-apply(f;x), can-apply(f;x), X(e), es-triggers(es;i;ds;conds), e  X, E, a:A fp B(a), ES, loc(e), a = b, kind(e), KindDeq, x  dom(f), p  q, Atom$n, if b then t else f fi , vartype(i;x), f(x)?z, IdDeq, @i discrete ds

Lemmas

es-state-subtype2, es-state-subtype, fpf-cap wf, id-deq wf, es-state-subtype-iff, eqtt to assert, assert of band, and functionality wrt iff, eqff to assert, bnot thru band, assert of bor, or functionality wrt iff, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, bor wf, fpf-dom wf, bnot wf, not wf, top wf, decl-state wf, assert wf, isl wf, pi2 wf, fpf-ap wf, es-state-when wf, es-val wf, false wf